i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), snd:msg-spec(ds; da).
msg-spec-loc-decl(snd; i; da)  msg-spec-loc(snd; i) 

latex

Definitions

IdLnk, t  T, x:A. B(x), msg-spec-links(snd), (x  l), source(l), <a, b>, Id, s = t, P  Q, x:AB(x), msg-spec-loc(snd; i), msg-spec-loc-decl(snd; i; da), Type, x. t(x), fpf(A; a.B(a)), Knd, msg-spec(ds; da), top, t.2, x.A(x), fpf-domain(f), x:A  B(x), t.1, msg-item(ds; da; k; l), type List, atom{$n:n}, x:A. B(x), b, P  Q, P  Q, guard(T), sq_type(T), prop{i:l}, sqequal(s; t), idlnk-deq, Kind-deq, product-deq(A; B; a; b), P  Q, left + right

Lemmas

member-fpf-domain, product-deq wf, Kind-deq wf, idlnk-deq wf, IdLnk sq, fpf-trivial-subtype-top, msg-item wf, pi1 wf, top wf, member map, fpf-domain wf, pi2 wf, msg-spec-loc-decl wf, msg-spec wf, Knd wf, fpf wf, Id wf, l member wf, msg-spec-links wf, IdLnk wf